Rose Tree Notes

module Rose where

data Rose a = Node a (Forest a)
  deriving Show

data Forest a = Empty | Cons (Rose a) (Forest a)
  deriving Show

{-

       5
      / \
     3   4

   Consider a standard tree type:

data Tree a = Leaf | Node a (Tree a) (Tree a)

Our tree would look like this:

  Node 5 (Node 3 Leaf Leaf) (Node 4 Leaf Leaf) :: Tree Int


As a Rose tree, it would look like this:

  Node 5 (Cons (Node 3 Empty) (Cons (Node 4 Empty) Empty)) :: Rose Int

 -}

-- Forests are basically just lists, so we could have done this:

data RoseAlt a = NodeAlt a [RoseAlt a]

-- Mutual induction

{- The Rose and Forest datatypes are *mutually recursive*:
     they are defined simultaneously, in terms of each other

   Therefore, the induction principle for rose trees will
    reflect this intertwined structure of the definition.
 -}

size :: Rose a -> Int
size(Node x f) = 1 + sizeF f
sizeF :: Forest a -> Int
sizeF Empty = 0
sizeF (Cons r f) = size r + sizeF f

height :: Rose a -> Int
height (Node x f) = 1 + heightF f
heightF :: Forest a -> Int
heightF Empty = 0
heightF (Cons r f) = max (height r) (heightF f)

-- Why are we doing this in a programming languages course?

-- A: induction is the #1 tool for proving properties about programming languages
--    ..because nearly all aspects of a programming language are built from
--      inductive definitions.
--        syntax trees are inductively defined
--        parsers are inductively defined
--        type systems are inductively defined
--        type checkers are inductively defined
--        compilers are inductively defined
--        the semantics of PLs are inductively defined
--        you name it!

data Expr = Num Int
          | Add Expr Expr
          | Mul Expr Expr
          | Var String deriving Show

{- 5 * (3 + x)                         -- concrete syntax

   Mul (Num 5) (Add (Num 3) (Var "x")) -- abstract syntax
 -}

-- We could insert this as a phase in our compiler
-- And we may want to prove that it does the right thing
constantFolder :: Expr -> Expr
constantFolder(Num n) = Num n
constantFolder(Var x) = Var x
constantFolder(Add e1 e2) =
  let e1' = constantFolder e1
      e2' = constantFolder e2
  in
    case (e1',e2') of
      (Num n, Num m) -> Num(n + m)
      _ -> Add e1' e2'
constantFolder(Mul e1 e2) =
  let e1' = constantFolder e1
      e2' = constantFolder e2
  in
    case (e1',e2') of
      (Num n, Num m) -> Num(n * m)
      _ -> Mul e1' e2'

{- To convince ourselves that our
   constant folder implementation
   never miscompiles,
   we may want to prove:

     value(e1) = value(constantFolder e1)

   Note: I haven't defined "value",
    nor will I until we get to the
    semantics part of the course

  Nonetheless, we'd have to proceed
  by structural induction on e1,
  and prove:


    the Num case,
    the Var case,
    the Add case,
    and the Mul case

 -}

In our case, we have:
  P(t) = height t ≤ size t
  Q(ts) = heightF ts ≤ sizeF ts


Theorem:
  (∀t. height t ≤ size t) ∧
  (∀ts. heightF ts ≤ sizeF ts)

Proof:
  by structural induction on t *and* ts.

Empty case:
  Prove: heightF Empty ≤ sizeF empty

  heightF Empty
  = 0             (by definition of heightF)
  = sizeF Empty   (by definition of sizeF)

Cons case:
  Prove: heightF(Cons t ts) ≤ sizeF(Cons t ts)
  Assuming the induction hypotheses:
    height t ≤ size t     (IH1)
    heightF ts ≤ sizeF ts (IH2)

  heightF(Cons t ts) = (by definition of heightF)
  max (height t) (heightF ts) ≤ (by arithmetic)
  height t + heightF ts ≤ (by IH1)
  size t + heightF ts ≤ (by IH2)
  size t + sizeF ts = (by definition sizeF)
  size(Cons t ts)

Rose case:
  Prove: height(Node x ts) ≤ size(Node x ts)
  Assuming the induction hypothesis:
    heightF ts ≤ sizeF ts (IH)

  height(Node x ts) = (by definition of heightF)
  1 + heightF ts ≤ (by IH)
  1 + sizeF ts = (by definition of sizeF)
  size(Node x ts)